Left Termination proof of /tmp/tmp1ufAot/binary.pl

Left Termination of the query pattern
add(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇒, 389 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 50 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 370 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 27 ms)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

    ↳23 PiDP

        ↳24 UsableRulesProof (⇔, 0 ms)

        ↳25 PiDP

        ↳26 PiDPToQDPProof (⇒, 12 ms)

        ↳27 QDP

        ↳28 QDPSizeChangeProof (⇔, 0 ms)

        ↳29 YES

(0) Obligation:

Clauses:

add(b, b, b).
add(X, b, X) :- binaryZ(X).
add(b, Y, Y) :- binaryZ(Y).
add(X, Y, Z) :- addz(X, Y, Z).
addx(one(X), b, one(X)) :- binary(X).
addx(zero(X), b, zero(X)) :- binaryZ(X).
addx(X, Y, Z) :- addz(X, Y, Z).
addy(b, one(Y), one(Y)) :- binary(Y).
addy(b, zero(Y), zero(Y)) :- binaryZ(Y).
addy(X, Y, Z) :- addz(X, Y, Z).
addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z).
addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z).
addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z).
addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z).
addc(b, b, one(b)).
addc(X, b, Z) :- succZ(X, Z).
addc(b, Y, Z) :- succZ(Y, Z).
addc(X, Y, Z) :- addC(X, Y, Z).
addX(zero(X), b, one(X)) :- binaryZ(X).
addX(one(X), b, zero(Z)) :- succ(X, Z).
addX(X, Y, Z) :- addC(X, Y, Z).
addY(b, zero(Y), one(Y)) :- binaryZ(Y).
addY(b, one(Y), zero(Z)) :- succ(Y, Z).
addY(X, Y, Z) :- addC(X, Y, Z).
addC(zero(X), zero(Y), one(Z)) :- addz(X, Y, Z).
addC(zero(X), one(Y), zero(Z)) :- addX(X, Y, Z).
addC(one(X), zero(Y), zero(Z)) :- addY(X, Y, Z).
addC(one(X), one(Y), one(Z)) :- addc(X, Y, Z).
binary(b).
binary(zero(X)) :- binaryZ(X).
binary(one(X)) :- binary(X).
binaryZ(zero(X)) :- binaryZ(X).
binaryZ(one(X)) :- binary(X).
succ(b, one(b)).
succ(zero(X), one(X)) :- binaryZ(X).
succ(one(X), zero(Z)) :- succ(X, Z).
succZ(zero(X), one(X)) :- binaryZ(X).
succZ(one(X), zero(Z)) :- succ(X, Z).
times(one(b), X, X).
times(zero(R), S, zero(RS)) :- times(R, S, RS).
times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS)).

Query: add(g,g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: add(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: add(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | add(b, b, T3), SCOPE: 1, CLAUSE: 1 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: add(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nadd(T1, T2, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: add(b, b, T3), SCOPE: 1, CLAUSE: 1 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: binaryZ(b) | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: binaryZ(b), SCOPE: 2, CLAUSE: 31 | binaryZ(b), SCOPE: 2, CLAUSE: 32 | ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: binaryZ(b), SCOPE: 2, CLAUSE: 32 | ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: add(b, b, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: binaryZ(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: binaryZ(b), SCOPE: 3, CLAUSE: 31 | binaryZ(b), SCOPE: 3, CLAUSE: 32\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: binaryZ(b), SCOPE: 3, CLAUSE: 32\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: addz(b, b, T8)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: addz(b, b, T8), SCOPE: 4, CLAUSE: 10 | addz(b, b, T8), SCOPE: 4, CLAUSE: 11 | addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: addz(b, b, T8), SCOPE: 4, CLAUSE: 11 | addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: binaryZ(b) | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nX41 is free\nadd(b, b, T3) !=? add(X2, b, X2)\nadd(b, b, T3) !=? add(b, X41, X41)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: binaryZ(b), SCOPE: 5, CLAUSE: 31 | binaryZ(b), SCOPE: 5, CLAUSE: 32 | ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: binaryZ(b), SCOPE: 5, CLAUSE: 32 | ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: addz(b, b, T13)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: addz(b, b, T16)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: addz(b, b, T16), SCOPE: 6, CLAUSE: 10 | addz(b, b, T16), SCOPE: 6, CLAUSE: 11 | addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: addz(b, b, T16), SCOPE: 6, CLAUSE: 11 | addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: binaryZ(T18) | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX78 is free\nadd(T1, T2, T3) !=? add(b, b, b)\nadd(T1, T2, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: binaryZ(T18), SCOPE: 7, CLAUSE: 31 | binaryZ(T18), SCOPE: 7, CLAUSE: 32 | ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: binaryZ(T18), SCOPE: 7, CLAUSE: 31\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: binaryZ(T18), SCOPE: 7, CLAUSE: 32 | ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: binaryZ(T23)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: binaryZ(T23), SCOPE: 8, CLAUSE: 31 | binaryZ(T23), SCOPE: 8, CLAUSE: 32\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: binaryZ(T23), SCOPE: 8, CLAUSE: 31\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: binaryZ(T23), SCOPE: 8, CLAUSE: 32\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: binaryZ(T29)\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: binary(T33)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: binary(T33), SCOPE: 9, CLAUSE: 28 | binary(T33), SCOPE: 9, CLAUSE: 29 | binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: binary(T33), SCOPE: 9, CLAUSE: 28\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: binary(T33), SCOPE: 9, CLAUSE: 29 | binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: binary(T33), SCOPE: 9, CLAUSE: 29\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: binaryZ(T38)\n\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: binary(T42)\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: binaryZ(T18), SCOPE: 7, CLAUSE: 32\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: binary(T47)\n\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: add(T18, b, T3), SCOPE: 1, CLAUSE: 2\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: binaryZ(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: addz(T54, b, T56)\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: addz(T54, b, T56), SCOPE: 10, CLAUSE: 10 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 11 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 12 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 13\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: addz(T54, b, T56), SCOPE: 10, CLAUSE: 11 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 12 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 13\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: addz(T54, b, T56), SCOPE: 10, CLAUSE: 12 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 13\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: addz(T54, b, T56), SCOPE: 10, CLAUSE: 13\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: binaryZ(T63) | add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX78 is free\nX142 is free\nadd(T1, T2, T3) !=? add(b, b, b)\nadd(T1, T2, T3) !=? add(X78, b, X78)\nadd(T1, T2, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: binaryZ(T63), SCOPE: 11, CLAUSE: 31 | binaryZ(T63), SCOPE: 11, CLAUSE: 32 | ?_11 | add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: binaryZ(T63), SCOPE: 11, CLAUSE: 31\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: binaryZ(T63), SCOPE: 11, CLAUSE: 32 | ?_11 | add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: binaryZ(T68)\n\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: binaryZ(T63), SCOPE: 11, CLAUSE: 32\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ?_11 | add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: binary(T74)\n\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: addz(b, T80, T82)\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: addz(b, T80, T82), SCOPE: 12, CLAUSE: 10 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 11 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 12 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 13\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: addz(b, T80, T82), SCOPE: 12, CLAUSE: 11 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 12 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 13\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: addz(b, T80, T82), SCOPE: 12, CLAUSE: 12 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 13\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: addz(b, T80, T82), SCOPE: 12, CLAUSE: 13\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: addz(T86, T87, T89)\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 10 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 11 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 12 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 13\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 10\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 11 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 12 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 13\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: addz(T102, T103, T105)\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 10 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 11 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 12 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 13\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 10\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 11 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 12 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 13\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: addz(T121, T122, T124)\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 11\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 12 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 13\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: addx(T140, T141, T143)\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 4 | addx(T140, T141, T143), SCOPE: 15, CLAUSE: 5 | addx(T140, T141, T143), SCOPE: 15, CLAUSE: 6\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 4\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 5 | addx(T140, T141, T143), SCOPE: 15, CLAUSE: 6\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: binary(T149)\n\nT149 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 5\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 6\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: binaryZ(T154)\n\nT154 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: addz(T166, T167, T169)\n\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 12\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 13\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: addy(T185, T186, T188)\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 7 | addy(T185, T186, T188), SCOPE: 16, CLAUSE: 8 | addy(T185, T186, T188), SCOPE: 16, CLAUSE: 9\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 7\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 8 | addy(T185, T186, T188), SCOPE: 16, CLAUSE: 9\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: binary(T194)\n\nT194 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 8\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 9\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: binaryZ(T199)\n\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: addz(T211, T212, T214)\n\nT211 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: addc(T224, T225, T227)\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 14 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 15 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 16 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 17\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 14\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 15 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 16 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 17\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 15\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 16 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 17\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: succZ(T236, T238)\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: succZ(T236, T238), SCOPE: 18, CLAUSE: 36 | succZ(T236, T238), SCOPE: 18, CLAUSE: 37\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: succZ(T236, T238), SCOPE: 18, CLAUSE: 36\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: succZ(T236, T238), SCOPE: 18, CLAUSE: 37\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: binaryZ(T244)\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: succ(T250, T252)\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: succ(T250, T252), SCOPE: 19, CLAUSE: 33 | succ(T250, T252), SCOPE: 19, CLAUSE: 34 | succ(T250, T252), SCOPE: 19, CLAUSE: 35\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: succ(T250, T252), SCOPE: 19, CLAUSE: 33\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: succ(T250, T252), SCOPE: 19, CLAUSE: 34 | succ(T250, T252), SCOPE: 19, CLAUSE: 35\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: succ(T250, T252), SCOPE: 19, CLAUSE: 34\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: succ(T250, T252), SCOPE: 19, CLAUSE: 35\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: binaryZ(T257)\n\nT257 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: succ(T263, T265)\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 16\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 17\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: succZ(T274, T276)\n\nT274 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: addC(T288, T289, T291)\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 24 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 25 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 26 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 27\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 24\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 25 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 26 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 27\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: addz(T307, T308, T310)\n\nT307 is ground\nT308 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 25\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 26 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 27\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: addX(T326, T327, T329)\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 18 | addX(T326, T327, T329), SCOPE: 21, CLAUSE: 19 | addX(T326, T327, T329), SCOPE: 21, CLAUSE: 20\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 18\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 19 | addX(T326, T327, T329), SCOPE: 21, CLAUSE: 20\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: binaryZ(T335)\n\nT335 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 19\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 20\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: succ(T345, T347)\n\nT345 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: addC(T358, T359, T361)\n\nT358 is ground\nT359 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 26\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 27\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: addY(T377, T378, T380)\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 21 | addY(T377, T378, T380), SCOPE: 22, CLAUSE: 22 | addY(T377, T378, T380), SCOPE: 22, CLAUSE: 23\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 21\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 22 | addY(T377, T378, T380), SCOPE: 22, CLAUSE: 23\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: binaryZ(T386)\n\nT386 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 22\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 23\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: succ(T396, T398)\n\nT396 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: addC(T409, T410, T412)\n\nT409 is ground\nT410 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: addc(T422, T423, T425)\n\nT422 is ground\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 11\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 12 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 13\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: addx(T438, T439, T441)\n\nT438 is ground\nT439 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 12\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 13\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: addy(T455, T456, T458)\n\nT455 is ground\nT456 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: addc(T466, T467, T469)\n\nT466 is ground\nT467 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 217 [arrowhead = none ];
217 -> 2;

218 [label="EVAL with clause\nadd(b, b, b).\nand substitutionT1 -> b,\nT2 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 218 [arrowhead = none ];
218 -> 3;

219 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 219 [arrowhead = none ];
219 -> 4;

220 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 220 [arrowhead = none ];
220 -> 5;

221 [label="EVAL with clause\nadd(X78, b, X78) :- binaryZ(X78).\nand substitutionT1 -> T18,\nX78 -> T18,\nT2 -> b,\nT3 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 221 [arrowhead = none ];
221 -> 38;

222 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 222 [arrowhead = none ];
222 -> 39;

223 [label="EVAL with clause\nadd(X2, b, X2) :- binaryZ(X2).\nand substitutionX2 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 223 [arrowhead = none ];
223 -> 6;

224 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 224 [arrowhead = none ];
224 -> 7;

225 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
6 -> 225 [arrowhead = none ];
225 -> 8;

226 [label="EVAL with clause\nadd(b, X41, X41) :- binaryZ(X41).\nand substitutionX41 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 226 [arrowhead = none ];
226 -> 25;

227 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 227 [arrowhead = none ];
227 -> 26;

228 [label="BACKTRACK\nfor clause: binaryZ(zero(X)) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 228 [arrowhead = none ];
228 -> 9;

229 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 229 [arrowhead = none ];
229 -> 10;

230 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 230 [arrowhead = none ];
230 -> 11;

231 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 231 [arrowhead = none ];
231 -> 12;

232 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 232 [arrowhead = none ];
232 -> 13;

233 [label="EVAL with clause\nadd(b, X9, X9) :- binaryZ(X9).\nand substitutionX9 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 233 [arrowhead = none ];
233 -> 14;

234 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 234 [arrowhead = none ];
234 -> 15;

235 [label="ONLY EVAL with clause\nadd(X22, X23, X24) :- addz(X22, X23, X24).\nand substitutionX22 -> b,\nX23 -> b,\nT3 -> T8,\nX24 -> T8,\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 235 [arrowhead = none ];
235 -> 19;

236 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
14 -> 236 [arrowhead = none ];
236 -> 16;

237 [label="BACKTRACK\nfor clause: binaryZ(zero(X)) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 237 [arrowhead = none ];
237 -> 17;

238 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 238 [arrowhead = none ];
238 -> 18;

239 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 239 [arrowhead = none ];
239 -> 20;

240 [label="BACKTRACK\nfor clause: addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 240 [arrowhead = none ];
240 -> 21;

241 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 241 [arrowhead = none ];
241 -> 22;

242 [label="BACKTRACK\nfor clause: addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 242 [arrowhead = none ];
242 -> 23;

243 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 243 [arrowhead = none ];
243 -> 24;

244 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
25 -> 244 [arrowhead = none ];
244 -> 27;

245 [label="ONLY EVAL with clause\nadd(X62, X63, X64) :- addz(X62, X63, X64).\nand substitutionX62 -> b,\nX63 -> b,\nT3 -> T16,\nX64 -> T16,\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 245 [arrowhead = none ];
245 -> 32;

246 [label="BACKTRACK\nfor clause: binaryZ(zero(X)) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 246 [arrowhead = none ];
246 -> 28;

247 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 247 [arrowhead = none ];
247 -> 29;

248 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 248 [arrowhead = none ];
248 -> 30;

249 [label="ONLY EVAL with clause\nadd(X53, X54, X55) :- addz(X53, X54, X55).\nand substitutionX53 -> b,\nX54 -> b,\nT3 -> T13,\nX55 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 249 [arrowhead = none ];
249 -> 31;

250 [label="INSTANCE with matching:\nT8 -> T13", fontsize=14, style = filled, fillcolor = lightgrey];
31 -> 250 [arrowhead = none , style=dashed];
250 -> 19[style=dashed];

251 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 251 [arrowhead = none ];
251 -> 33;

252 [label="BACKTRACK\nfor clause: addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 252 [arrowhead = none ];
252 -> 34;

253 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 253 [arrowhead = none ];
253 -> 35;

254 [label="BACKTRACK\nfor clause: addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 254 [arrowhead = none ];
254 -> 36;

255 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 255 [arrowhead = none ];
255 -> 37;

256 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
38 -> 256 [arrowhead = none ];
256 -> 40;

257 [label="EVAL with clause\nadd(b, X142, X142) :- binaryZ(X142).\nand substitutionT1 -> b,\nT2 -> T63,\nX142 -> T63,\nT3 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 257 [arrowhead = none ];
257 -> 79;

258 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 258 [arrowhead = none ];
258 -> 80;

259 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 259 [arrowhead = none ];
259 -> 41;

260 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 260 [arrowhead = none ];
260 -> 42;

261 [label="EVAL with clause\nbinaryZ(zero(X83)) :- binaryZ(X83).\nand substitutionX83 -> T23,\nT18 -> zero(T23)", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 261 [arrowhead = none ];
261 -> 43;

262 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 262 [arrowhead = none ];
262 -> 44;

263 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 263 [arrowhead = none ];
263 -> 64;

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 264 [arrowhead = none ];
264 -> 65;

265 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 265 [arrowhead = none ];
265 -> 45;

266 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 266 [arrowhead = none ];
266 -> 46;

267 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 267 [arrowhead = none ];
267 -> 47;

268 [label="EVAL with clause\nbinaryZ(zero(X89)) :- binaryZ(X89).\nand substitutionX89 -> T29,\nT23 -> zero(T29)", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 268 [arrowhead = none ];
268 -> 48;

269 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 269 [arrowhead = none ];
269 -> 49;

270 [label="EVAL with clause\nbinaryZ(one(X93)) :- binary(X93).\nand substitutionX93 -> T33,\nT23 -> one(T33)", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 270 [arrowhead = none ];
270 -> 50;

271 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 271 [arrowhead = none ];
271 -> 51;

272 [label="INSTANCE with matching:\nT23 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 272 [arrowhead = none , style=dashed];
272 -> 43[style=dashed];

273 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
50 -> 273 [arrowhead = none ];
273 -> 52;

274 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 274 [arrowhead = none ];
274 -> 53;

275 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 275 [arrowhead = none ];
275 -> 54;

276 [label="EVAL with clause\nbinary(b).\nand substitutionT33 -> b", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 276 [arrowhead = none ];
276 -> 55;

277 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 277 [arrowhead = none ];
277 -> 56;

278 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 278 [arrowhead = none ];
278 -> 58;

279 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 279 [arrowhead = none ];
279 -> 59;

280 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 280 [arrowhead = none ];
280 -> 57;

281 [label="EVAL with clause\nbinary(zero(X98)) :- binaryZ(X98).\nand substitutionX98 -> T38,\nT33 -> zero(T38)", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 281 [arrowhead = none ];
281 -> 60;

282 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 282 [arrowhead = none ];
282 -> 61;

283 [label="EVAL with clause\nbinary(one(X102)) :- binary(X102).\nand substitutionX102 -> T42,\nT33 -> one(T42)", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 283 [arrowhead = none ];
283 -> 62;

284 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 284 [arrowhead = none ];
284 -> 63;

285 [label="INSTANCE with matching:\nT23 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 285 [arrowhead = none , style=dashed];
285 -> 43[style=dashed];

286 [label="INSTANCE with matching:\nT33 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 286 [arrowhead = none , style=dashed];
286 -> 50[style=dashed];

287 [label="EVAL with clause\nbinaryZ(one(X107)) :- binary(X107).\nand substitutionX107 -> T47,\nT18 -> one(T47)", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 287 [arrowhead = none ];
287 -> 66;

288 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 288 [arrowhead = none ];
288 -> 67;

289 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 289 [arrowhead = none ];
289 -> 68;

290 [label="INSTANCE with matching:\nT33 -> T47", fontsize=14, style = filled, fillcolor = lightgrey];
66 -> 290 [arrowhead = none , style=dashed];
290 -> 50[style=dashed];

291 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 291 [arrowhead = none ];
291 -> 69;

292 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 292 [arrowhead = none ];
292 -> 70;

293 [label="EVAL with clause\nadd(b, X112, X112) :- binaryZ(X112).\nand substitutionT18 -> b,\nX112 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 293 [arrowhead = none ];
293 -> 71;

294 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 294 [arrowhead = none ];
294 -> 72;

295 [label="ONLY EVAL with clause\nadd(X123, X124, X125) :- addz(X123, X124, X125).\nand substitutionT18 -> T54,\nX123 -> T54,\nX124 -> b,\nT3 -> T56,\nX125 -> T56,\nT55 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 295 [arrowhead = none ];
295 -> 73;

296 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 296 [arrowhead = none , style=dashed];
296 -> 14[style=dashed];

297 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
73 -> 297 [arrowhead = none ];
297 -> 74;

298 [label="BACKTRACK\nfor clause: addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 298 [arrowhead = none ];
298 -> 75;

299 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 299 [arrowhead = none ];
299 -> 76;

300 [label="BACKTRACK\nfor clause: addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 300 [arrowhead = none ];
300 -> 77;

301 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 301 [arrowhead = none ];
301 -> 78;

302 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
79 -> 302 [arrowhead = none ];
302 -> 81;

303 [label="ONLY EVAL with clause\nadd(X184, X185, X186) :- addz(X184, X185, X186).\nand substitutionT1 -> T86,\nX184 -> T86,\nT2 -> T87,\nX185 -> T87,\nT3 -> T89,\nX186 -> T89,\nT88 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 303 [arrowhead = none ];
303 -> 97;

304 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
81 -> 304 [arrowhead = none ];
304 -> 82;

305 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
81 -> 305 [arrowhead = none ];
305 -> 83;

306 [label="EVAL with clause\nbinaryZ(zero(X147)) :- binaryZ(X147).\nand substitutionX147 -> T68,\nT63 -> zero(T68)", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 306 [arrowhead = none ];
306 -> 84;

307 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 307 [arrowhead = none ];
307 -> 85;

308 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 308 [arrowhead = none ];
308 -> 86;

309 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 309 [arrowhead = none ];
309 -> 87;

310 [label="INSTANCE with matching:\nT23 -> T68", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 310 [arrowhead = none , style=dashed];
310 -> 43[style=dashed];

311 [label="EVAL with clause\nbinaryZ(one(X153)) :- binary(X153).\nand substitutionX153 -> T74,\nT63 -> one(T74)", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 311 [arrowhead = none ];
311 -> 88;

312 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 312 [arrowhead = none ];
312 -> 89;

313 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 313 [arrowhead = none ];
313 -> 90;

314 [label="INSTANCE with matching:\nT33 -> T74", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 314 [arrowhead = none , style=dashed];
314 -> 50[style=dashed];

315 [label="ONLY EVAL with clause\nadd(X163, X164, X165) :- addz(X163, X164, X165).\nand substitutionX163 -> b,\nT63 -> T80,\nX164 -> T80,\nT3 -> T82,\nX165 -> T82,\nT81 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 315 [arrowhead = none ];
315 -> 91;

316 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 316 [arrowhead = none ];
316 -> 92;

317 [label="BACKTRACK\nfor clause: addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 317 [arrowhead = none ];
317 -> 93;

318 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 318 [arrowhead = none ];
318 -> 94;

319 [label="BACKTRACK\nfor clause: addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 319 [arrowhead = none ];
319 -> 95;

320 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 320 [arrowhead = none ];
320 -> 96;

321 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
97 -> 321 [arrowhead = none ];
321 -> 98;

322 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 322 [arrowhead = none ];
322 -> 99;

323 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 323 [arrowhead = none ];
323 -> 100;

324 [label="EVAL with clause\naddz(zero(X199), zero(X200), zero(X201)) :- addz(X199, X200, X201).\nand substitutionX199 -> T102,\nT86 -> zero(T102),\nX200 -> T103,\nT87 -> zero(T103),\nX201 -> T105,\nT89 -> zero(T105),\nT104 -> T105", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 324 [arrowhead = none ];
324 -> 101;

325 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 325 [arrowhead = none ];
325 -> 102;

326 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
100 -> 326 [arrowhead = none ];
326 -> 207;

327 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
100 -> 327 [arrowhead = none ];
327 -> 208;

328 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
101 -> 328 [arrowhead = none ];
328 -> 103;

329 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
103 -> 329 [arrowhead = none ];
329 -> 104;

330 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
103 -> 330 [arrowhead = none ];
330 -> 105;

331 [label="EVAL with clause\naddz(zero(X217), zero(X218), zero(X219)) :- addz(X217, X218, X219).\nand substitutionX217 -> T121,\nT102 -> zero(T121),\nX218 -> T122,\nT103 -> zero(T122),\nX219 -> T124,\nT105 -> zero(T124),\nT123 -> T124", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 331 [arrowhead = none ];
331 -> 106;

332 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 332 [arrowhead = none ];
332 -> 107;

333 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
105 -> 333 [arrowhead = none ];
333 -> 108;

334 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
105 -> 334 [arrowhead = none ];
334 -> 109;

335 [label="INSTANCE with matching:\nT102 -> T121\nT103 -> T122\nT105 -> T124", fontsize=14, style = filled, fillcolor = lightgrey];
106 -> 335 [arrowhead = none , style=dashed];
335 -> 101[style=dashed];

336 [label="EVAL with clause\naddz(zero(X235), one(X236), one(X237)) :- addx(X235, X236, X237).\nand substitutionX235 -> T140,\nT102 -> zero(T140),\nX236 -> T141,\nT103 -> one(T141),\nX237 -> T143,\nT105 -> one(T143),\nT142 -> T143", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 336 [arrowhead = none ];
336 -> 110;

337 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 337 [arrowhead = none ];
337 -> 111;

338 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
109 -> 338 [arrowhead = none ];
338 -> 122;

339 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
109 -> 339 [arrowhead = none ];
339 -> 123;

340 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
110 -> 340 [arrowhead = none ];
340 -> 112;

341 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 341 [arrowhead = none ];
341 -> 113;

342 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 342 [arrowhead = none ];
342 -> 114;

343 [label="EVAL with clause\naddx(one(X243), b, one(X243)) :- binary(X243).\nand substitutionX243 -> T149,\nT140 -> one(T149),\nT141 -> b,\nT143 -> one(T149)", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 343 [arrowhead = none ];
343 -> 115;

344 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 344 [arrowhead = none ];
344 -> 116;

345 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
114 -> 345 [arrowhead = none ];
345 -> 117;

346 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
114 -> 346 [arrowhead = none ];
346 -> 118;

347 [label="INSTANCE with matching:\nT33 -> T149", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 347 [arrowhead = none , style=dashed];
347 -> 50[style=dashed];

348 [label="EVAL with clause\naddx(zero(X248), b, zero(X248)) :- binaryZ(X248).\nand substitutionX248 -> T154,\nT140 -> zero(T154),\nT141 -> b,\nT143 -> zero(T154)", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 348 [arrowhead = none ];
348 -> 119;

349 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 349 [arrowhead = none ];
349 -> 120;

350 [label="ONLY EVAL with clause\naddx(X259, X260, X261) :- addz(X259, X260, X261).\nand substitutionT140 -> T166,\nX259 -> T166,\nT141 -> T167,\nX260 -> T167,\nT143 -> T169,\nX261 -> T169,\nT168 -> T169", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 350 [arrowhead = none ];
350 -> 121;

351 [label="INSTANCE with matching:\nT23 -> T154", fontsize=14, style = filled, fillcolor = lightgrey];
119 -> 351 [arrowhead = none , style=dashed];
351 -> 43[style=dashed];

352 [label="INSTANCE with matching:\nT102 -> T166\nT103 -> T167\nT105 -> T169", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 352 [arrowhead = none , style=dashed];
352 -> 101[style=dashed];

353 [label="EVAL with clause\naddz(one(X277), zero(X278), one(X279)) :- addy(X277, X278, X279).\nand substitutionX277 -> T185,\nT102 -> one(T185),\nX278 -> T186,\nT103 -> zero(T186),\nX279 -> T188,\nT105 -> one(T188),\nT187 -> T188", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 353 [arrowhead = none ];
353 -> 124;

354 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 354 [arrowhead = none ];
354 -> 125;

355 [label="EVAL with clause\naddz(one(X313), one(X314), zero(X315)) :- addc(X313, X314, X315).\nand substitutionX313 -> T224,\nT102 -> one(T224),\nX314 -> T225,\nT103 -> one(T225),\nX315 -> T227,\nT105 -> zero(T227),\nT226 -> T227", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 355 [arrowhead = none ];
355 -> 136;

356 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 356 [arrowhead = none ];
356 -> 137;

357 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
124 -> 357 [arrowhead = none ];
357 -> 126;

358 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 358 [arrowhead = none ];
358 -> 127;

359 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 359 [arrowhead = none ];
359 -> 128;

360 [label="EVAL with clause\naddy(b, one(X285), one(X285)) :- binary(X285).\nand substitutionT185 -> b,\nX285 -> T194,\nT186 -> one(T194),\nT188 -> one(T194)", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 360 [arrowhead = none ];
360 -> 129;

361 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 361 [arrowhead = none ];
361 -> 130;

362 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
128 -> 362 [arrowhead = none ];
362 -> 131;

363 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
128 -> 363 [arrowhead = none ];
363 -> 132;

364 [label="INSTANCE with matching:\nT33 -> T194", fontsize=14, style = filled, fillcolor = lightgrey];
129 -> 364 [arrowhead = none , style=dashed];
364 -> 50[style=dashed];

365 [label="EVAL with clause\naddy(b, zero(X290), zero(X290)) :- binaryZ(X290).\nand substitutionT185 -> b,\nX290 -> T199,\nT186 -> zero(T199),\nT188 -> zero(T199)", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 365 [arrowhead = none ];
365 -> 133;

366 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
131 -> 366 [arrowhead = none ];
366 -> 134;

367 [label="ONLY EVAL with clause\naddy(X301, X302, X303) :- addz(X301, X302, X303).\nand substitutionT185 -> T211,\nX301 -> T211,\nT186 -> T212,\nX302 -> T212,\nT188 -> T214,\nX303 -> T214,\nT213 -> T214", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 367 [arrowhead = none ];
367 -> 135;

368 [label="INSTANCE with matching:\nT23 -> T199", fontsize=14, style = filled, fillcolor = lightgrey];
133 -> 368 [arrowhead = none , style=dashed];
368 -> 43[style=dashed];

369 [label="INSTANCE with matching:\nT102 -> T211\nT103 -> T212\nT105 -> T214", fontsize=14, style = filled, fillcolor = lightgrey];
135 -> 369 [arrowhead = none , style=dashed];
369 -> 101[style=dashed];

370 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
136 -> 370 [arrowhead = none ];
370 -> 138;

371 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 371 [arrowhead = none ];
371 -> 139;

372 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 372 [arrowhead = none ];
372 -> 140;

373 [label="EVAL with clause\naddc(b, b, one(b)).\nand substitutionT224 -> b,\nT225 -> b,\nT227 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 373 [arrowhead = none ];
373 -> 141;

374 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 374 [arrowhead = none ];
374 -> 142;

375 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
140 -> 375 [arrowhead = none ];
375 -> 144;

376 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
140 -> 376 [arrowhead = none ];
376 -> 145;

377 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 377 [arrowhead = none ];
377 -> 143;

378 [label="EVAL with clause\naddc(X324, b, X325) :- succZ(X324, X325).\nand substitutionT224 -> T236,\nX324 -> T236,\nT225 -> b,\nT227 -> T238,\nX325 -> T238,\nT237 -> T238", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 378 [arrowhead = none ];
378 -> 146;

379 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 379 [arrowhead = none ];
379 -> 147;

380 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
145 -> 380 [arrowhead = none ];
380 -> 167;

381 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
145 -> 381 [arrowhead = none ];
381 -> 168;

382 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
146 -> 382 [arrowhead = none ];
382 -> 148;

383 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
148 -> 383 [arrowhead = none ];
383 -> 149;

384 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
148 -> 384 [arrowhead = none ];
384 -> 150;

385 [label="EVAL with clause\nsuccZ(zero(X331), one(X331)) :- binaryZ(X331).\nand substitutionX331 -> T244,\nT236 -> zero(T244),\nT238 -> one(T244)", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 385 [arrowhead = none ];
385 -> 151;

386 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 386 [arrowhead = none ];
386 -> 152;

387 [label="EVAL with clause\nsuccZ(one(X337), zero(X338)) :- succ(X337, X338).\nand substitutionX337 -> T250,\nT236 -> one(T250),\nX338 -> T252,\nT238 -> zero(T252),\nT251 -> T252", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 387 [arrowhead = none ];
387 -> 153;

388 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
150 -> 388 [arrowhead = none ];
388 -> 154;

389 [label="INSTANCE with matching:\nT23 -> T244", fontsize=14, style = filled, fillcolor = lightgrey];
151 -> 389 [arrowhead = none , style=dashed];
389 -> 43[style=dashed];

390 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
153 -> 390 [arrowhead = none ];
390 -> 155;

391 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
155 -> 391 [arrowhead = none ];
391 -> 156;

392 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
155 -> 392 [arrowhead = none ];
392 -> 157;

393 [label="EVAL with clause\nsucc(b, one(b)).\nand substitutionT250 -> b,\nT252 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 393 [arrowhead = none ];
393 -> 158;

394 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
156 -> 394 [arrowhead = none ];
394 -> 159;

395 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
157 -> 395 [arrowhead = none ];
395 -> 161;

396 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
157 -> 396 [arrowhead = none ];
396 -> 162;

397 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 397 [arrowhead = none ];
397 -> 160;

398 [label="EVAL with clause\nsucc(zero(X343), one(X343)) :- binaryZ(X343).\nand substitutionX343 -> T257,\nT250 -> zero(T257),\nT252 -> one(T257)", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 398 [arrowhead = none ];
398 -> 163;

399 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
161 -> 399 [arrowhead = none ];
399 -> 164;

400 [label="EVAL with clause\nsucc(one(X349), zero(X350)) :- succ(X349, X350).\nand substitutionX349 -> T263,\nT250 -> one(T263),\nX350 -> T265,\nT252 -> zero(T265),\nT264 -> T265", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 400 [arrowhead = none ];
400 -> 165;

401 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
162 -> 401 [arrowhead = none ];
401 -> 166;

402 [label="INSTANCE with matching:\nT23 -> T257", fontsize=14, style = filled, fillcolor = lightgrey];
163 -> 402 [arrowhead = none , style=dashed];
402 -> 43[style=dashed];

403 [label="INSTANCE with matching:\nT250 -> T263\nT252 -> T265", fontsize=14, style = filled, fillcolor = lightgrey];
165 -> 403 [arrowhead = none , style=dashed];
403 -> 153[style=dashed];

404 [label="EVAL with clause\naddc(b, X359, X360) :- succZ(X359, X360).\nand substitutionT224 -> b,\nT225 -> T274,\nX359 -> T274,\nT227 -> T276,\nX360 -> T276,\nT275 -> T276", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 404 [arrowhead = none ];
404 -> 169;

405 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
167 -> 405 [arrowhead = none ];
405 -> 170;

406 [label="ONLY EVAL with clause\naddc(X371, X372, X373) :- addC(X371, X372, X373).\nand substitutionT224 -> T288,\nX371 -> T288,\nT225 -> T289,\nX372 -> T289,\nT227 -> T291,\nX373 -> T291,\nT290 -> T291", fontsize=14, style = filled, fillcolor = lightblue];
168 -> 406 [arrowhead = none ];
406 -> 171;

407 [label="INSTANCE with matching:\nT236 -> T274\nT238 -> T276", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 407 [arrowhead = none , style=dashed];
407 -> 146[style=dashed];

408 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
171 -> 408 [arrowhead = none ];
408 -> 172;

409 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
172 -> 409 [arrowhead = none ];
409 -> 173;

410 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
172 -> 410 [arrowhead = none ];
410 -> 174;

411 [label="EVAL with clause\naddC(zero(X389), zero(X390), one(X391)) :- addz(X389, X390, X391).\nand substitutionX389 -> T307,\nT288 -> zero(T307),\nX390 -> T308,\nT289 -> zero(T308),\nX391 -> T310,\nT291 -> one(T310),\nT309 -> T310", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 411 [arrowhead = none ];
411 -> 175;

412 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 412 [arrowhead = none ];
412 -> 176;

413 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
174 -> 413 [arrowhead = none ];
413 -> 177;

414 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
174 -> 414 [arrowhead = none ];
414 -> 178;

415 [label="INSTANCE with matching:\nT102 -> T307\nT103 -> T308\nT105 -> T310", fontsize=14, style = filled, fillcolor = lightgrey];
175 -> 415 [arrowhead = none , style=dashed];
415 -> 101[style=dashed];

416 [label="EVAL with clause\naddC(zero(X407), one(X408), zero(X409)) :- addX(X407, X408, X409).\nand substitutionX407 -> T326,\nT288 -> zero(T326),\nX408 -> T327,\nT289 -> one(T327),\nX409 -> T329,\nT291 -> zero(T329),\nT328 -> T329", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 416 [arrowhead = none ];
416 -> 179;

417 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 417 [arrowhead = none ];
417 -> 180;

418 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
178 -> 418 [arrowhead = none ];
418 -> 191;

419 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
178 -> 419 [arrowhead = none ];
419 -> 192;

420 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
179 -> 420 [arrowhead = none ];
420 -> 181;

421 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
181 -> 421 [arrowhead = none ];
421 -> 182;

422 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
181 -> 422 [arrowhead = none ];
422 -> 183;

423 [label="EVAL with clause\naddX(zero(X415), b, one(X415)) :- binaryZ(X415).\nand substitutionX415 -> T335,\nT326 -> zero(T335),\nT327 -> b,\nT329 -> one(T335)", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 423 [arrowhead = none ];
423 -> 184;

424 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 424 [arrowhead = none ];
424 -> 185;

425 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
183 -> 425 [arrowhead = none ];
425 -> 186;

426 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
183 -> 426 [arrowhead = none ];
426 -> 187;

427 [label="INSTANCE with matching:\nT23 -> T335", fontsize=14, style = filled, fillcolor = lightgrey];
184 -> 427 [arrowhead = none , style=dashed];
427 -> 43[style=dashed];

428 [label="EVAL with clause\naddX(one(X425), b, zero(X426)) :- succ(X425, X426).\nand substitutionX425 -> T345,\nT326 -> one(T345),\nT327 -> b,\nX426 -> T347,\nT329 -> zero(T347),\nT346 -> T347", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 428 [arrowhead = none ];
428 -> 188;

429 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
186 -> 429 [arrowhead = none ];
429 -> 189;

430 [label="ONLY EVAL with clause\naddX(X436, X437, X438) :- addC(X436, X437, X438).\nand substitutionT326 -> T358,\nX436 -> T358,\nT327 -> T359,\nX437 -> T359,\nT329 -> T361,\nX438 -> T361,\nT360 -> T361", fontsize=14, style = filled, fillcolor = lightblue];
187 -> 430 [arrowhead = none ];
430 -> 190;

431 [label="INSTANCE with matching:\nT250 -> T345\nT252 -> T347", fontsize=14, style = filled, fillcolor = lightgrey];
188 -> 431 [arrowhead = none , style=dashed];
431 -> 153[style=dashed];

432 [label="INSTANCE with matching:\nT288 -> T358\nT289 -> T359\nT291 -> T361", fontsize=14, style = filled, fillcolor = lightgrey];
190 -> 432 [arrowhead = none , style=dashed];
432 -> 171[style=dashed];

433 [label="EVAL with clause\naddC(one(X454), zero(X455), zero(X456)) :- addY(X454, X455, X456).\nand substitutionX454 -> T377,\nT288 -> one(T377),\nX455 -> T378,\nT289 -> zero(T378),\nX456 -> T380,\nT291 -> zero(T380),\nT379 -> T380", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 433 [arrowhead = none ];
433 -> 193;

434 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
191 -> 434 [arrowhead = none ];
434 -> 194;

435 [label="EVAL with clause\naddC(one(X495), one(X496), one(X497)) :- addc(X495, X496, X497).\nand substitutionX495 -> T422,\nT288 -> one(T422),\nX496 -> T423,\nT289 -> one(T423),\nX497 -> T425,\nT291 -> one(T425),\nT424 -> T425", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 435 [arrowhead = none ];
435 -> 205;

436 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
192 -> 436 [arrowhead = none ];
436 -> 206;

437 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
193 -> 437 [arrowhead = none ];
437 -> 195;

438 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 438 [arrowhead = none ];
438 -> 196;

439 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 439 [arrowhead = none ];
439 -> 197;

440 [label="EVAL with clause\naddY(b, zero(X462), one(X462)) :- binaryZ(X462).\nand substitutionT377 -> b,\nX462 -> T386,\nT378 -> zero(T386),\nT380 -> one(T386)", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 440 [arrowhead = none ];
440 -> 198;

441 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 441 [arrowhead = none ];
441 -> 199;

442 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
197 -> 442 [arrowhead = none ];
442 -> 200;

443 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
197 -> 443 [arrowhead = none ];
443 -> 201;

444 [label="INSTANCE with matching:\nT23 -> T386", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 444 [arrowhead = none , style=dashed];
444 -> 43[style=dashed];

445 [label="EVAL with clause\naddY(b, one(X472), zero(X473)) :- succ(X472, X473).\nand substitutionT377 -> b,\nX472 -> T396,\nT378 -> one(T396),\nX473 -> T398,\nT380 -> zero(T398),\nT397 -> T398", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 445 [arrowhead = none ];
445 -> 202;

446 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 446 [arrowhead = none ];
446 -> 203;

447 [label="ONLY EVAL with clause\naddY(X483, X484, X485) :- addC(X483, X484, X485).\nand substitutionT377 -> T409,\nX483 -> T409,\nT378 -> T410,\nX484 -> T410,\nT380 -> T412,\nX485 -> T412,\nT411 -> T412", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 447 [arrowhead = none ];
447 -> 204;

448 [label="INSTANCE with matching:\nT250 -> T396\nT252 -> T398", fontsize=14, style = filled, fillcolor = lightgrey];
202 -> 448 [arrowhead = none , style=dashed];
448 -> 153[style=dashed];

449 [label="INSTANCE with matching:\nT288 -> T409\nT289 -> T410\nT291 -> T412", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 449 [arrowhead = none , style=dashed];
449 -> 171[style=dashed];

450 [label="INSTANCE with matching:\nT224 -> T422\nT225 -> T423\nT227 -> T425", fontsize=14, style = filled, fillcolor = lightgrey];
205 -> 450 [arrowhead = none , style=dashed];
450 -> 136[style=dashed];

451 [label="EVAL with clause\naddz(zero(X510), one(X511), one(X512)) :- addx(X510, X511, X512).\nand substitutionX510 -> T438,\nT86 -> zero(T438),\nX511 -> T439,\nT87 -> one(T439),\nX512 -> T441,\nT89 -> one(T441),\nT440 -> T441", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 451 [arrowhead = none ];
451 -> 209;

452 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
207 -> 452 [arrowhead = none ];
452 -> 210;

453 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
208 -> 453 [arrowhead = none ];
453 -> 211;

454 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
208 -> 454 [arrowhead = none ];
454 -> 212;

455 [label="INSTANCE with matching:\nT140 -> T438\nT141 -> T439\nT143 -> T441", fontsize=14, style = filled, fillcolor = lightgrey];
209 -> 455 [arrowhead = none , style=dashed];
455 -> 110[style=dashed];

456 [label="EVAL with clause\naddz(one(X526), zero(X527), one(X528)) :- addy(X526, X527, X528).\nand substitutionX526 -> T455,\nT86 -> one(T455),\nX527 -> T456,\nT87 -> zero(T456),\nX528 -> T458,\nT89 -> one(T458),\nT457 -> T458", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 456 [arrowhead = none ];
456 -> 213;

457 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
211 -> 457 [arrowhead = none ];
457 -> 214;

458 [label="EVAL with clause\naddz(one(X536), one(X537), zero(X538)) :- addc(X536, X537, X538).\nand substitutionX536 -> T466,\nT86 -> one(T466),\nX537 -> T467,\nT87 -> one(T467),\nX538 -> T469,\nT89 -> zero(T469),\nT468 -> T469", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 458 [arrowhead = none ];
458 -> 215;

459 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
212 -> 459 [arrowhead = none ];
459 -> 216;

460 [label="INSTANCE with matching:\nT185 -> T455\nT186 -> T456\nT188 -> T458", fontsize=14, style = filled, fillcolor = lightgrey];
213 -> 460 [arrowhead = none , style=dashed];
460 -> 124[style=dashed];

461 [label="INSTANCE with matching:\nT224 -> T466\nT225 -> T467\nT227 -> T469", fontsize=14, style = filled, fillcolor = lightgrey];
215 -> 461 [arrowhead = none , style=dashed];
461 -> 136[style=dashed];

}

(2) Obligation:

Clauses:

binaryZA(zero(T29)) :- binaryZA(T29).
binaryZA(one(T33)) :- binaryB(T33).
binaryB(b).
binaryB(zero(T38)) :- binaryZA(T38).
binaryB(one(T42)) :- binaryB(T42).
addzC(zero(T121), zero(T122), zero(T124)) :- addzC(T121, T122, T124).
addzC(zero(T140), one(T141), one(T143)) :- addxD(T140, T141, T143).
addzC(one(T185), zero(T186), one(T188)) :- addyE(T185, T186, T188).
addzC(one(T224), one(T225), zero(T227)) :- addcF(T224, T225, T227).
succG(b, one(b)).
succG(zero(T257), one(T257)) :- binaryZA(T257).
succG(one(T263), zero(T265)) :- succG(T263, T265).
succZH(zero(T244), one(T244)) :- binaryZA(T244).
succZH(one(T250), zero(T252)) :- succG(T250, T252).
addCI(zero(T307), zero(T308), one(T310)) :- addzC(T307, T308, T310).
addCI(zero(zero(T335)), one(b), zero(one(T335))) :- binaryZA(T335).
addCI(zero(one(T345)), one(b), zero(zero(T347))) :- succG(T345, T347).
addCI(zero(T358), one(T359), zero(T361)) :- addCI(T358, T359, T361).
addCI(one(b), zero(zero(T386)), zero(one(T386))) :- binaryZA(T386).
addCI(one(b), zero(one(T396)), zero(zero(T398))) :- succG(T396, T398).
addCI(one(T409), zero(T410), zero(T412)) :- addCI(T409, T410, T412).
addCI(one(T422), one(T423), one(T425)) :- addcF(T422, T423, T425).
addcF(b, b, one(b)).
addcF(T236, b, T238) :- succZH(T236, T238).
addcF(b, T274, T276) :- succZH(T274, T276).
addcF(T288, T289, T291) :- addCI(T288, T289, T291).
addxD(one(T149), b, one(T149)) :- binaryB(T149).
addxD(zero(T154), b, zero(T154)) :- binaryZA(T154).
addxD(T166, T167, T169) :- addzC(T166, T167, T169).
addyE(b, one(T194), one(T194)) :- binaryB(T194).
addyE(b, zero(T199), zero(T199)) :- binaryZA(T199).
addyE(T211, T212, T214) :- addzC(T211, T212, T214).
addJ(b, b, b).
addJ(zero(T23), b, zero(T23)) :- binaryZA(T23).
addJ(one(T47), b, one(T47)) :- binaryB(T47).
addJ(b, zero(T68), zero(T68)) :- binaryZA(T68).
addJ(b, one(T74), one(T74)) :- binaryB(T74).
addJ(zero(T102), zero(T103), zero(T105)) :- addzC(T102, T103, T105).
addJ(zero(T438), one(T439), one(T441)) :- addxD(T438, T439, T441).
addJ(one(T455), zero(T456), one(T458)) :- addyE(T455, T456, T458).
addJ(one(T466), one(T467), zero(T469)) :- addcF(T466, T467, T469).

Query: addJ(g,g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
addJ_in: (b,b,f)
binaryZA_in: (b)
binaryB_in: (b)
addzC_in: (b,b,f)
addxD_in: (b,b,f)
addyE_in: (b,b,f)
addcF_in: (b,b,f)
succZH_in: (b,f)
succG_in: (b,f)
addCI_in: (b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

ADDJ_IN_GGA(zero(T23), b, zero(T23)) → U30_GGA(T23, binaryZA_in_g(T23))
ADDJ_IN_GGA(zero(T23), b, zero(T23)) → BINARYZA_IN_G(T23)
BINARYZA_IN_G(zero(T29)) → U1_G(T29, binaryZA_in_g(T29))
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYZA_IN_G(one(T33)) → U2_G(T33, binaryB_in_g(T33))
BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → U3_G(T38, binaryZA_in_g(T38))
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYB_IN_G(one(T42)) → U4_G(T42, binaryB_in_g(T42))
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)
ADDJ_IN_GGA(one(T47), b, one(T47)) → U31_GGA(T47, binaryB_in_g(T47))
ADDJ_IN_GGA(one(T47), b, one(T47)) → BINARYB_IN_G(T47)
ADDJ_IN_GGA(b, zero(T68), zero(T68)) → U32_GGA(T68, binaryZA_in_g(T68))
ADDJ_IN_GGA(b, zero(T68), zero(T68)) → BINARYZA_IN_G(T68)
ADDJ_IN_GGA(b, one(T74), one(T74)) → U33_GGA(T74, binaryB_in_g(T74))
ADDJ_IN_GGA(b, one(T74), one(T74)) → BINARYB_IN_G(T74)
ADDJ_IN_GGA(zero(T102), zero(T103), zero(T105)) → U34_GGA(T102, T103, T105, addzC_in_gga(T102, T103, T105))
ADDJ_IN_GGA(zero(T102), zero(T103), zero(T105)) → ADDZC_IN_GGA(T102, T103, T105)
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → U5_GGA(T121, T122, T124, addzC_in_gga(T121, T122, T124))
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZC_IN_GGA(T121, T122, T124)
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → U6_GGA(T140, T141, T143, addxD_in_gga(T140, T141, T143))
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXD_IN_GGA(T140, T141, T143)
ADDXD_IN_GGA(one(T149), b, one(T149)) → U24_GGA(T149, binaryB_in_g(T149))
ADDXD_IN_GGA(one(T149), b, one(T149)) → BINARYB_IN_G(T149)
ADDXD_IN_GGA(zero(T154), b, zero(T154)) → U25_GGA(T154, binaryZA_in_g(T154))
ADDXD_IN_GGA(zero(T154), b, zero(T154)) → BINARYZA_IN_G(T154)
ADDXD_IN_GGA(T166, T167, T169) → U26_GGA(T166, T167, T169, addzC_in_gga(T166, T167, T169))
ADDXD_IN_GGA(T166, T167, T169) → ADDZC_IN_GGA(T166, T167, T169)
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → U7_GGA(T185, T186, T188, addyE_in_gga(T185, T186, T188))
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYE_IN_GGA(T185, T186, T188)
ADDYE_IN_GGA(b, one(T194), one(T194)) → U27_GGA(T194, binaryB_in_g(T194))
ADDYE_IN_GGA(b, one(T194), one(T194)) → BINARYB_IN_G(T194)
ADDYE_IN_GGA(b, zero(T199), zero(T199)) → U28_GGA(T199, binaryZA_in_g(T199))
ADDYE_IN_GGA(b, zero(T199), zero(T199)) → BINARYZA_IN_G(T199)
ADDYE_IN_GGA(T211, T212, T214) → U29_GGA(T211, T212, T214, addzC_in_gga(T211, T212, T214))
ADDYE_IN_GGA(T211, T212, T214) → ADDZC_IN_GGA(T211, T212, T214)
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → U8_GGA(T224, T225, T227, addcF_in_gga(T224, T225, T227))
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCF_IN_GGA(T224, T225, T227)
ADDCF_IN_GGA(T236, b, T238) → U21_GGA(T236, T238, succZH_in_ga(T236, T238))
ADDCF_IN_GGA(T236, b, T238) → SUCCZH_IN_GA(T236, T238)
SUCCZH_IN_GA(zero(T244), one(T244)) → U11_GA(T244, binaryZA_in_g(T244))
SUCCZH_IN_GA(zero(T244), one(T244)) → BINARYZA_IN_G(T244)
SUCCZH_IN_GA(one(T250), zero(T252)) → U12_GA(T250, T252, succG_in_ga(T250, T252))
SUCCZH_IN_GA(one(T250), zero(T252)) → SUCCG_IN_GA(T250, T252)
SUCCG_IN_GA(zero(T257), one(T257)) → U9_GA(T257, binaryZA_in_g(T257))
SUCCG_IN_GA(zero(T257), one(T257)) → BINARYZA_IN_G(T257)
SUCCG_IN_GA(one(T263), zero(T265)) → U10_GA(T263, T265, succG_in_ga(T263, T265))
SUCCG_IN_GA(one(T263), zero(T265)) → SUCCG_IN_GA(T263, T265)
ADDCF_IN_GGA(b, T274, T276) → U22_GGA(T274, T276, succZH_in_ga(T274, T276))
ADDCF_IN_GGA(b, T274, T276) → SUCCZH_IN_GA(T274, T276)
ADDCF_IN_GGA(T288, T289, T291) → U23_GGA(T288, T289, T291, addCI_in_gga(T288, T289, T291))
ADDCF_IN_GGA(T288, T289, T291) → ADDCI_IN_GGA(T288, T289, T291)
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → U13_GGA(T307, T308, T310, addzC_in_gga(T307, T308, T310))
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZC_IN_GGA(T307, T308, T310)
ADDCI_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → U14_GGA(T335, binaryZA_in_g(T335))
ADDCI_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → BINARYZA_IN_G(T335)
ADDCI_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → U15_GGA(T345, T347, succG_in_ga(T345, T347))
ADDCI_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → SUCCG_IN_GA(T345, T347)
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → U16_GGA(T358, T359, T361, addCI_in_gga(T358, T359, T361))
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCI_IN_GGA(T358, T359, T361)
ADDCI_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → U17_GGA(T386, binaryZA_in_g(T386))
ADDCI_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → BINARYZA_IN_G(T386)
ADDCI_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → U18_GGA(T396, T398, succG_in_ga(T396, T398))
ADDCI_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → SUCCG_IN_GA(T396, T398)
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → U19_GGA(T409, T410, T412, addCI_in_gga(T409, T410, T412))
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCI_IN_GGA(T409, T410, T412)
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → U20_GGA(T422, T423, T425, addcF_in_gga(T422, T423, T425))
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → ADDCF_IN_GGA(T422, T423, T425)
ADDJ_IN_GGA(zero(T438), one(T439), one(T441)) → U35_GGA(T438, T439, T441, addxD_in_gga(T438, T439, T441))
ADDJ_IN_GGA(zero(T438), one(T439), one(T441)) → ADDXD_IN_GGA(T438, T439, T441)
ADDJ_IN_GGA(one(T455), zero(T456), one(T458)) → U36_GGA(T455, T456, T458, addyE_in_gga(T455, T456, T458))
ADDJ_IN_GGA(one(T455), zero(T456), one(T458)) → ADDYE_IN_GGA(T455, T456, T458)
ADDJ_IN_GGA(one(T466), one(T467), zero(T469)) → U37_GGA(T466, T467, T469, addcF_in_gga(T466, T467, T469))
ADDJ_IN_GGA(one(T466), one(T467), zero(T469)) → ADDCF_IN_GGA(T466, T467, T469)

The TRS R consists of the following rules:

addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))

The argument filtering Pi contains the following mapping:
addJ_in_gga(x1, x2, x3) = addJ_in_gga(x1, x2)
b = b
addJ_out_gga(x1, x2, x3) = addJ_out_gga(x1, x2, x3)
zero(x1) = zero(x1)
U30_gga(x1, x2) = U30_gga(x1, x2)
binaryZA_in_g(x1) = binaryZA_in_g(x1)
U1_g(x1, x2) = U1_g(x1, x2)
one(x1) = one(x1)
U2_g(x1, x2) = U2_g(x1, x2)
binaryB_in_g(x1) = binaryB_in_g(x1)
binaryB_out_g(x1) = binaryB_out_g(x1)
U3_g(x1, x2) = U3_g(x1, x2)
binaryZA_out_g(x1) = binaryZA_out_g(x1)
U4_g(x1, x2) = U4_g(x1, x2)
U31_gga(x1, x2) = U31_gga(x1, x2)
U32_gga(x1, x2) = U32_gga(x1, x2)
U33_gga(x1, x2) = U33_gga(x1, x2)
U34_gga(x1, x2, x3, x4) = U34_gga(x1, x2, x4)
addzC_in_gga(x1, x2, x3) = addzC_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4) = U5_gga(x1, x2, x4)
U6_gga(x1, x2, x3, x4) = U6_gga(x1, x2, x4)
addxD_in_gga(x1, x2, x3) = addxD_in_gga(x1, x2)
U24_gga(x1, x2) = U24_gga(x1, x2)
addxD_out_gga(x1, x2, x3) = addxD_out_gga(x1, x2, x3)
U25_gga(x1, x2) = U25_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x2, x4)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
addyE_in_gga(x1, x2, x3) = addyE_in_gga(x1, x2)
U27_gga(x1, x2) = U27_gga(x1, x2)
addyE_out_gga(x1, x2, x3) = addyE_out_gga(x1, x2, x3)
U28_gga(x1, x2) = U28_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x2, x4)
U8_gga(x1, x2, x3, x4) = U8_gga(x1, x2, x4)
addcF_in_gga(x1, x2, x3) = addcF_in_gga(x1, x2)
addcF_out_gga(x1, x2, x3) = addcF_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3) = U21_gga(x1, x3)
succZH_in_ga(x1, x2) = succZH_in_ga(x1)
U11_ga(x1, x2) = U11_ga(x1, x2)
succZH_out_ga(x1, x2) = succZH_out_ga(x1, x2)
U12_ga(x1, x2, x3) = U12_ga(x1, x3)
succG_in_ga(x1, x2) = succG_in_ga(x1)
succG_out_ga(x1, x2) = succG_out_ga(x1, x2)
U9_ga(x1, x2) = U9_ga(x1, x2)
U10_ga(x1, x2, x3) = U10_ga(x1, x3)
U22_gga(x1, x2, x3) = U22_gga(x1, x3)
U23_gga(x1, x2, x3, x4) = U23_gga(x1, x2, x4)
addCI_in_gga(x1, x2, x3) = addCI_in_gga(x1, x2)
U13_gga(x1, x2, x3, x4) = U13_gga(x1, x2, x4)
addzC_out_gga(x1, x2, x3) = addzC_out_gga(x1, x2, x3)
addCI_out_gga(x1, x2, x3) = addCI_out_gga(x1, x2, x3)
U14_gga(x1, x2) = U14_gga(x1, x2)
U15_gga(x1, x2, x3) = U15_gga(x1, x3)
U16_gga(x1, x2, x3, x4) = U16_gga(x1, x2, x4)
U17_gga(x1, x2) = U17_gga(x1, x2)
U18_gga(x1, x2, x3) = U18_gga(x1, x3)
U19_gga(x1, x2, x3, x4) = U19_gga(x1, x2, x4)
U20_gga(x1, x2, x3, x4) = U20_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4) = U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4) = U36_gga(x1, x2, x4)
U37_gga(x1, x2, x3, x4) = U37_gga(x1, x2, x4)
ADDJ_IN_GGA(x1, x2, x3) = ADDJ_IN_GGA(x1, x2)
U30_GGA(x1, x2) = U30_GGA(x1, x2)
BINARYZA_IN_G(x1) = BINARYZA_IN_G(x1)
U1_G(x1, x2) = U1_G(x1, x2)
U2_G(x1, x2) = U2_G(x1, x2)
BINARYB_IN_G(x1) = BINARYB_IN_G(x1)
U3_G(x1, x2) = U3_G(x1, x2)
U4_G(x1, x2) = U4_G(x1, x2)
U31_GGA(x1, x2) = U31_GGA(x1, x2)
U32_GGA(x1, x2) = U32_GGA(x1, x2)
U33_GGA(x1, x2) = U33_GGA(x1, x2)
U34_GGA(x1, x2, x3, x4) = U34_GGA(x1, x2, x4)
ADDZC_IN_GGA(x1, x2, x3) = ADDZC_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4) = U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4) = U6_GGA(x1, x2, x4)
ADDXD_IN_GGA(x1, x2, x3) = ADDXD_IN_GGA(x1, x2)
U24_GGA(x1, x2) = U24_GGA(x1, x2)
U25_GGA(x1, x2) = U25_GGA(x1, x2)
U26_GGA(x1, x2, x3, x4) = U26_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4) = U7_GGA(x1, x2, x4)
ADDYE_IN_GGA(x1, x2, x3) = ADDYE_IN_GGA(x1, x2)
U27_GGA(x1, x2) = U27_GGA(x1, x2)
U28_GGA(x1, x2) = U28_GGA(x1, x2)
U29_GGA(x1, x2, x3, x4) = U29_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4) = U8_GGA(x1, x2, x4)
ADDCF_IN_GGA(x1, x2, x3) = ADDCF_IN_GGA(x1, x2)
U21_GGA(x1, x2, x3) = U21_GGA(x1, x3)
SUCCZH_IN_GA(x1, x2) = SUCCZH_IN_GA(x1)
U11_GA(x1, x2) = U11_GA(x1, x2)
U12_GA(x1, x2, x3) = U12_GA(x1, x3)
SUCCG_IN_GA(x1, x2) = SUCCG_IN_GA(x1)
U9_GA(x1, x2) = U9_GA(x1, x2)
U10_GA(x1, x2, x3) = U10_GA(x1, x3)
U22_GGA(x1, x2, x3) = U22_GGA(x1, x3)
U23_GGA(x1, x2, x3, x4) = U23_GGA(x1, x2, x4)
ADDCI_IN_GGA(x1, x2, x3) = ADDCI_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4) = U13_GGA(x1, x2, x4)
U14_GGA(x1, x2) = U14_GGA(x1, x2)
U15_GGA(x1, x2, x3) = U15_GGA(x1, x3)
U16_GGA(x1, x2, x3, x4) = U16_GGA(x1, x2, x4)
U17_GGA(x1, x2) = U17_GGA(x1, x2)
U18_GGA(x1, x2, x3) = U18_GGA(x1, x3)
U19_GGA(x1, x2, x3, x4) = U19_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3, x4) = U20_GGA(x1, x2, x4)
U35_GGA(x1, x2, x3, x4) = U35_GGA(x1, x2, x4)
U36_GGA(x1, x2, x3, x4) = U36_GGA(x1, x2, x4)
U37_GGA(x1, x2, x3, x4) = U37_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDJ_IN_GGA(zero(T23), b, zero(T23)) → U30_GGA(T23, binaryZA_in_g(T23))
ADDJ_IN_GGA(zero(T23), b, zero(T23)) → BINARYZA_IN_G(T23)
BINARYZA_IN_G(zero(T29)) → U1_G(T29, binaryZA_in_g(T29))
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYZA_IN_G(one(T33)) → U2_G(T33, binaryB_in_g(T33))
BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → U3_G(T38, binaryZA_in_g(T38))
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYB_IN_G(one(T42)) → U4_G(T42, binaryB_in_g(T42))
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)
ADDJ_IN_GGA(one(T47), b, one(T47)) → U31_GGA(T47, binaryB_in_g(T47))
ADDJ_IN_GGA(one(T47), b, one(T47)) → BINARYB_IN_G(T47)
ADDJ_IN_GGA(b, zero(T68), zero(T68)) → U32_GGA(T68, binaryZA_in_g(T68))
ADDJ_IN_GGA(b, zero(T68), zero(T68)) → BINARYZA_IN_G(T68)
ADDJ_IN_GGA(b, one(T74), one(T74)) → U33_GGA(T74, binaryB_in_g(T74))
ADDJ_IN_GGA(b, one(T74), one(T74)) → BINARYB_IN_G(T74)
ADDJ_IN_GGA(zero(T102), zero(T103), zero(T105)) → U34_GGA(T102, T103, T105, addzC_in_gga(T102, T103, T105))
ADDJ_IN_GGA(zero(T102), zero(T103), zero(T105)) → ADDZC_IN_GGA(T102, T103, T105)
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → U5_GGA(T121, T122, T124, addzC_in_gga(T121, T122, T124))
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZC_IN_GGA(T121, T122, T124)
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → U6_GGA(T140, T141, T143, addxD_in_gga(T140, T141, T143))
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXD_IN_GGA(T140, T141, T143)
ADDXD_IN_GGA(one(T149), b, one(T149)) → U24_GGA(T149, binaryB_in_g(T149))
ADDXD_IN_GGA(one(T149), b, one(T149)) → BINARYB_IN_G(T149)
ADDXD_IN_GGA(zero(T154), b, zero(T154)) → U25_GGA(T154, binaryZA_in_g(T154))
ADDXD_IN_GGA(zero(T154), b, zero(T154)) → BINARYZA_IN_G(T154)
ADDXD_IN_GGA(T166, T167, T169) → U26_GGA(T166, T167, T169, addzC_in_gga(T166, T167, T169))
ADDXD_IN_GGA(T166, T167, T169) → ADDZC_IN_GGA(T166, T167, T169)
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → U7_GGA(T185, T186, T188, addyE_in_gga(T185, T186, T188))
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYE_IN_GGA(T185, T186, T188)
ADDYE_IN_GGA(b, one(T194), one(T194)) → U27_GGA(T194, binaryB_in_g(T194))
ADDYE_IN_GGA(b, one(T194), one(T194)) → BINARYB_IN_G(T194)
ADDYE_IN_GGA(b, zero(T199), zero(T199)) → U28_GGA(T199, binaryZA_in_g(T199))
ADDYE_IN_GGA(b, zero(T199), zero(T199)) → BINARYZA_IN_G(T199)
ADDYE_IN_GGA(T211, T212, T214) → U29_GGA(T211, T212, T214, addzC_in_gga(T211, T212, T214))
ADDYE_IN_GGA(T211, T212, T214) → ADDZC_IN_GGA(T211, T212, T214)
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → U8_GGA(T224, T225, T227, addcF_in_gga(T224, T225, T227))
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCF_IN_GGA(T224, T225, T227)
ADDCF_IN_GGA(T236, b, T238) → U21_GGA(T236, T238, succZH_in_ga(T236, T238))
ADDCF_IN_GGA(T236, b, T238) → SUCCZH_IN_GA(T236, T238)
SUCCZH_IN_GA(zero(T244), one(T244)) → U11_GA(T244, binaryZA_in_g(T244))
SUCCZH_IN_GA(zero(T244), one(T244)) → BINARYZA_IN_G(T244)
SUCCZH_IN_GA(one(T250), zero(T252)) → U12_GA(T250, T252, succG_in_ga(T250, T252))
SUCCZH_IN_GA(one(T250), zero(T252)) → SUCCG_IN_GA(T250, T252)
SUCCG_IN_GA(zero(T257), one(T257)) → U9_GA(T257, binaryZA_in_g(T257))
SUCCG_IN_GA(zero(T257), one(T257)) → BINARYZA_IN_G(T257)
SUCCG_IN_GA(one(T263), zero(T265)) → U10_GA(T263, T265, succG_in_ga(T263, T265))
SUCCG_IN_GA(one(T263), zero(T265)) → SUCCG_IN_GA(T263, T265)
ADDCF_IN_GGA(b, T274, T276) → U22_GGA(T274, T276, succZH_in_ga(T274, T276))
ADDCF_IN_GGA(b, T274, T276) → SUCCZH_IN_GA(T274, T276)
ADDCF_IN_GGA(T288, T289, T291) → U23_GGA(T288, T289, T291, addCI_in_gga(T288, T289, T291))
ADDCF_IN_GGA(T288, T289, T291) → ADDCI_IN_GGA(T288, T289, T291)
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → U13_GGA(T307, T308, T310, addzC_in_gga(T307, T308, T310))
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZC_IN_GGA(T307, T308, T310)
ADDCI_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → U14_GGA(T335, binaryZA_in_g(T335))
ADDCI_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → BINARYZA_IN_G(T335)
ADDCI_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → U15_GGA(T345, T347, succG_in_ga(T345, T347))
ADDCI_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → SUCCG_IN_GA(T345, T347)
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → U16_GGA(T358, T359, T361, addCI_in_gga(T358, T359, T361))
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCI_IN_GGA(T358, T359, T361)
ADDCI_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → U17_GGA(T386, binaryZA_in_g(T386))
ADDCI_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → BINARYZA_IN_G(T386)
ADDCI_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → U18_GGA(T396, T398, succG_in_ga(T396, T398))
ADDCI_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → SUCCG_IN_GA(T396, T398)
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → U19_GGA(T409, T410, T412, addCI_in_gga(T409, T410, T412))
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCI_IN_GGA(T409, T410, T412)
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → U20_GGA(T422, T423, T425, addcF_in_gga(T422, T423, T425))
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → ADDCF_IN_GGA(T422, T423, T425)
ADDJ_IN_GGA(zero(T438), one(T439), one(T441)) → U35_GGA(T438, T439, T441, addxD_in_gga(T438, T439, T441))
ADDJ_IN_GGA(zero(T438), one(T439), one(T441)) → ADDXD_IN_GGA(T438, T439, T441)
ADDJ_IN_GGA(one(T455), zero(T456), one(T458)) → U36_GGA(T455, T456, T458, addyE_in_gga(T455, T456, T458))
ADDJ_IN_GGA(one(T455), zero(T456), one(T458)) → ADDYE_IN_GGA(T455, T456, T458)
ADDJ_IN_GGA(one(T466), one(T467), zero(T469)) → U37_GGA(T466, T467, T469, addcF_in_gga(T466, T467, T469))
ADDJ_IN_GGA(one(T466), one(T467), zero(T469)) → ADDCF_IN_GGA(T466, T467, T469)

The TRS R consists of the following rules:

addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 58 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)

The TRS R consists of the following rules:

addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
The graph contains the following edges 1 > 1
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)
The graph contains the following edges 1 > 1
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
The graph contains the following edges 1 > 1
BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUCCG_IN_GA(one(T263), zero(T265)) → SUCCG_IN_GA(T263, T265)

The TRS R consists of the following rules:

addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUCCG_IN_GA(one(T263), zero(T265)) → SUCCG_IN_GA(T263, T265)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
SUCCG_IN_GA(x1, x2) = SUCCG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUCCG_IN_GA(one(T263)) → SUCCG_IN_GA(T263)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

SUCCG_IN_GA(one(T263)) → SUCCG_IN_GA(T263)
The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDXD_IN_GGA(T166, T167, T169) → ADDZC_IN_GGA(T166, T167, T169)
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZC_IN_GGA(T121, T122, T124)
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXD_IN_GGA(T140, T141, T143)
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYE_IN_GGA(T185, T186, T188)
ADDYE_IN_GGA(T211, T212, T214) → ADDZC_IN_GGA(T211, T212, T214)
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCF_IN_GGA(T224, T225, T227)
ADDCF_IN_GGA(T288, T289, T291) → ADDCI_IN_GGA(T288, T289, T291)
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZC_IN_GGA(T307, T308, T310)
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCI_IN_GGA(T358, T359, T361)
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCI_IN_GGA(T409, T410, T412)
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → ADDCF_IN_GGA(T422, T423, T425)

The TRS R consists of the following rules:

addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDXD_IN_GGA(T166, T167, T169) → ADDZC_IN_GGA(T166, T167, T169)
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZC_IN_GGA(T121, T122, T124)
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXD_IN_GGA(T140, T141, T143)
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYE_IN_GGA(T185, T186, T188)
ADDYE_IN_GGA(T211, T212, T214) → ADDZC_IN_GGA(T211, T212, T214)
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCF_IN_GGA(T224, T225, T227)
ADDCF_IN_GGA(T288, T289, T291) → ADDCI_IN_GGA(T288, T289, T291)
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZC_IN_GGA(T307, T308, T310)
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCI_IN_GGA(T358, T359, T361)
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCI_IN_GGA(T409, T410, T412)
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → ADDCF_IN_GGA(T422, T423, T425)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
ADDZC_IN_GGA(x1, x2, x3) = ADDZC_IN_GGA(x1, x2)
ADDXD_IN_GGA(x1, x2, x3) = ADDXD_IN_GGA(x1, x2)
ADDYE_IN_GGA(x1, x2, x3) = ADDYE_IN_GGA(x1, x2)
ADDCF_IN_GGA(x1, x2, x3) = ADDCF_IN_GGA(x1, x2)
ADDCI_IN_GGA(x1, x2, x3) = ADDCI_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADDXD_IN_GGA(T166, T167) → ADDZC_IN_GGA(T166, T167)
ADDZC_IN_GGA(zero(T121), zero(T122)) → ADDZC_IN_GGA(T121, T122)
ADDZC_IN_GGA(zero(T140), one(T141)) → ADDXD_IN_GGA(T140, T141)
ADDZC_IN_GGA(one(T185), zero(T186)) → ADDYE_IN_GGA(T185, T186)
ADDYE_IN_GGA(T211, T212) → ADDZC_IN_GGA(T211, T212)
ADDZC_IN_GGA(one(T224), one(T225)) → ADDCF_IN_GGA(T224, T225)
ADDCF_IN_GGA(T288, T289) → ADDCI_IN_GGA(T288, T289)
ADDCI_IN_GGA(zero(T307), zero(T308)) → ADDZC_IN_GGA(T307, T308)
ADDCI_IN_GGA(zero(T358), one(T359)) → ADDCI_IN_GGA(T358, T359)
ADDCI_IN_GGA(one(T409), zero(T410)) → ADDCI_IN_GGA(T409, T410)
ADDCI_IN_GGA(one(T422), one(T423)) → ADDCF_IN_GGA(T422, T423)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ADDZC_IN_GGA(zero(T140), one(T141)) → ADDXD_IN_GGA(T140, T141)
The graph contains the following edges 1 > 1, 2 > 2
ADDZC_IN_GGA(zero(T121), zero(T122)) → ADDZC_IN_GGA(T121, T122)
The graph contains the following edges 1 > 1, 2 > 2
ADDXD_IN_GGA(T166, T167) → ADDZC_IN_GGA(T166, T167)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDYE_IN_GGA(T211, T212) → ADDZC_IN_GGA(T211, T212)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDCI_IN_GGA(zero(T307), zero(T308)) → ADDZC_IN_GGA(T307, T308)
The graph contains the following edges 1 > 1, 2 > 2
ADDZC_IN_GGA(one(T185), zero(T186)) → ADDYE_IN_GGA(T185, T186)
The graph contains the following edges 1 > 1, 2 > 2
ADDZC_IN_GGA(one(T224), one(T225)) → ADDCF_IN_GGA(T224, T225)
The graph contains the following edges 1 > 1, 2 > 2
ADDCF_IN_GGA(T288, T289) → ADDCI_IN_GGA(T288, T289)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDCI_IN_GGA(one(T422), one(T423)) → ADDCF_IN_GGA(T422, T423)
The graph contains the following edges 1 > 1, 2 > 2
ADDCI_IN_GGA(zero(T358), one(T359)) → ADDCI_IN_GGA(T358, T359)
The graph contains the following edges 1 > 1, 2 > 2
ADDCI_IN_GGA(one(T409), zero(T410)) → ADDCI_IN_GGA(T409, T410)
The graph contains the following edges 1 > 1, 2 > 2

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) QDPSizeChangeProof (EQUIVALENT transformation)

(29) YES